Inference at * 1 1 1 
Iof proof for Lemma comp nat ind a:



1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. 
4. s : 
5. s < 0
  P(s) 

latex

 by % S type empty % (Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t
 ) inil_term) 

latex

 .

Definitions

False, A, A  B, P  Q,